// Copyright 2012 Google Inc. All Rights Reserved.
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
//     http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

#include "stp_worker.h"

#include <sys/socket.h>
#include <sys/wait.h>

#include "expr/Assignment.h"
#include "expr/Constraints.h"
#include "expr/Expr.h"
#include "expr/ExprBuilder.h"
#include "expr/ExprUtil.h"
#include "expr/ExprPPrinter.h"
#include "expr/Parser.h"
#include "glog/logging.h"
#include "llvm/ADT/OwningPtr.h"
#include "llvm/Support/CommandLine.h"
#include "llvm/Support/ManagedStatic.h"
#include "llvm/Support/MemoryBuffer.h"
#include "llvm/Support/raw_ostream.h"
#include "llvm/Support/system_error.h"
#include "solver/Solver.h"
#include "util/Ref.h"

namespace seven_summits {
namespace {
enum BuilderKinds {
  DefaultBuilder,
  ConstantFoldingBuilder,
  SimplifyingBuilder
};

llvm::cl::opt<BuilderKinds>
clBuilderKind("builder",
            llvm::cl::desc("Expression builder:"),
            llvm::cl::init(DefaultBuilder),
            llvm::cl::values(
            clEnumValN(DefaultBuilder, "default",
                       "Default expression construction."),
            clEnumValN(ConstantFoldingBuilder, "constant-folding",
                       "Fold constant expressions."),
            clEnumValN(SimplifyingBuilder, "simplify",
                       "Fold constants and simplify expressions."),
            clEnumValEnd));
} // namespace anonymous

using expr::ExprBuilder;

using expr::ref;
using expr::Array;
using expr::Assignment;
using expr::AssignmentEvaluator;
using expr::ConstraintManager;  // in "expr/Constraints.h"
using expr::ConstantExpr;
using expr::Decl;
using expr::Expr;
using expr::ExprBuilder;
using expr::Parser;
using expr::QueryCommand;
using solver::Query;  // in "expr/Solver.h"
using solver::Solver;
using solver::STPSolver;



using ::llvm::dyn_cast;
using ::llvm::MemoryBuffer;
using ::llvm::OwningPtr;
using ::llvm::StringRef;

ExprBuilder* getExprBuilder() {
  ExprBuilder* exprBuilder;
  switch (clBuilderKind) {
    case DefaultBuilder:
      exprBuilder = expr::createDefaultExprBuilder();
      break;
    case ConstantFoldingBuilder:
      exprBuilder = expr::createDefaultExprBuilder();
      exprBuilder = expr::createConstantFoldingExprBuilder(exprBuilder);
      break;
    case SimplifyingBuilder:
      exprBuilder = expr::createDefaultExprBuilder();
      exprBuilder = expr::createConstantFoldingExprBuilder(exprBuilder);
      exprBuilder = expr::createSimplifyingExprBuilder(exprBuilder);
      break;
  }
  return exprBuilder;
}

StpWorker::StpWorker()
    : builder_(getExprBuilder()) {}

StpWorker::~StpWorker() {}

void solve(QueryCommand *qc, SmtResponse* resp) {
  Solver *S = new STPSolver(false);

  if (qc->Values.empty() && qc->Objects.empty()) {
    bool provably_true;
    if (S->mustBeTrue(Query(ConstraintManager(qc->Constraints), qc->Query),
                      provably_true)) {
      resp->set_status(SmtResponse::OK);
      resp->set_verdict(provably_true
                        ? SmtResponse::VALID
                        : SmtResponse::INVALID);
    } else {
      resp->set_status(SmtResponse::OTHER_FAILURE);
    }
    return;
  }

  if (!qc->Values.empty()) {
    if (!qc->Objects.empty() || qc->Values.size() > 1 ||
        !qc->Query->isFalse()) {
      // no support for counterexamples -- todo(upstream kleaver)
      VLOG(2) << "Not implemented.";
      resp->set_status(SmtResponse::NOT_IMPLEMENTED);
      return;
    }

    ref<ConstantExpr> result;
    if (S->getValue(Query(ConstraintManager(qc->Constraints),
                          qc->Values[0]),
                    result)) {
      resp->set_status(SmtResponse::OK);
      resp->set_verdict(SmtResponse::INVALID);
      uint64_t value = result->getZExtValue();
      unsigned char *valueptr = (unsigned char *) &value;
      // Write result
      SmtResponse::Assignment* assignment = resp->add_assignment();
      assignment->set_index(0);
      for (int i = result->getWidth(); i >= 0; i--) {
        assignment->add_value(valueptr[i]);
      }
    } else {
      resp->set_status(SmtResponse::OTHER_FAILURE);
    }
    return;
  }

  std::vector< std::vector<unsigned char> > result;
  ConstraintManager originalCM = ConstraintManager(qc->Constraints);
  Query origQuery = Query(originalCM, qc->Query);

  if (S->getInitialValues(origQuery, qc->Objects, result)) {
    resp->set_status(SmtResponse::OK);
    resp->set_verdict(SmtResponse::INVALID);

    for (unsigned i = 0, e = result.size(); i != e; ++i) {
      SmtResponse::Assignment* assignment = resp->add_assignment();
      assignment->set_index(i);
      for (unsigned j = 0; j != qc->Objects[i]->size; ++j) {
        assignment->add_value(result[i][j]);
      }
    }
  } else {  // no satisfying assignment
    resp->set_status(SmtResponse::OK);
    resp->set_verdict(SmtResponse::INVALID);
  }
}

void StpWorker::Solve() {
  int sv[2];
  if (pipe(sv) < 0) {
    LOG(ERROR) << "could not open create a pipe";
    response()->set_status(SmtResponse::OTHER_FAILURE);
    return;
  }
  ExprBuilder* builder = getExprBuilder();
  const int pid = fork();
  if (pid == -1) {
    LOG(ERROR) << "could not fork";
    response()->set_status(SmtResponse::OTHER_FAILURE);
    return;
  }

  if (pid == 0) {
    close(sv[0]);
    OwningPtr<MemoryBuffer> query(MemoryBuffer::getMemBuffer(
        StringRef(request().query())));
    bool success = true;
    std::vector<Decl*> decls;
    QueryCommand* qc = NULL;
    Parser* parser = Parser::Create("", query.get(), builder);
    parser->SetMaxErrors(20);
    while (Decl *decl = parser->ParseTopLevelDecl()) {
      decls.push_back(decl);
      if (QueryCommand *tmpqc = dyn_cast<QueryCommand>(decl)) {
        if (qc == NULL) {
          qc = tmpqc;
        } else {
          // Ensure we have a single query
          success = false;
        }
      }
    }
    // TODO: this will simply crash the server on invalid syntax.
    // also treat restrictions like "array domain must be w8" as failure
    if (parser->GetNumErrors() == 0) {
      solve(qc, response());
    } else {
      response()->set_status(SmtResponse::PARSE_FAILURE);
    }
    response()->SerializeToFileDescriptor(sv[1]);
    for (std::vector<Decl*>::iterator it = decls.begin(); it != decls.end(); ++it) {
      delete *it;
    }
    delete parser;
    close(sv[1]);

    exit(0);
  } else {
    close(sv[1]);
    int status;
    pid_t res;

    do {
      /// TODO: timeout
      res = waitpid(pid, &status, 0);
    } while (res < 0 && errno == EINTR);

    response()->ParseFromFileDescriptor(sv[0]);
    close(sv[0]);
  }
}

}  // namespace seven_summits
